\begin{tabbing}
$\forall$$A$, $B$:Type.
\\[0ex]AtomFree(Type;$A$)
\\[0ex]$\Rightarrow$ AtomFree(Type;$B$)
\\[0ex]$\Rightarrow$ (\=$\forall$${\it eq}$:EqDecider($A$).\+
\\[0ex]AtomFree(EqDecider($A$);${\it eq}$)
\\[0ex]$\Rightarrow$ (\=$\forall$$f$:$a$:$A$ fp$\rightarrow$ $B$.\+
\\[0ex]($\forall$$a$:$A$. AtomFree($A$;$a$))
\\[0ex]$\Rightarrow$ $\forall$$a$$\in$dom($f$). $x$=$f$($a$) $\Rightarrow$  AtomFree($B$;$x$)
\\[0ex]$\Rightarrow$ AtomFree($a$:$A$ fp$\rightarrow$ $B$;$f$)))
\-\-
\end{tabbing}